/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.ArrayList;
import java.util.List;

import alloy.ast.ArrowMultExpr;
import alloy.ast.LeafId;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.SetMultExpr;
import alloy.bool.BooleanFormula;
import alloy.type.RelationType;
import alloy.util.MultiDimArray;
import alloy.util.MultiDimIter;
import alloy.util.Util;

/**
 * Allocates Boolean variables to represent which relations have which
 * tuples in the solution, trying to allocate as few Boolean variables
 * as needed.
 */
public class CompactRelationAllocator extends DefaultRelationAllocator {
    /**
     * Side conditions: if you have a scalar set of scope 3 and represent it
     * with two Boolean variables, we need the constraint that the two Boolean variables represent
     * a binary number less than 3.  {@link List} of {@link BooleanFormula} conjuncts.
     */
    private List /* of BooleanFormula */ _sideConditions = new ArrayList();

    //////////////
    // Methods //
    ////////////

    public CompactRelationAllocator(ASTInfo astInfo_,
                    BoolVarAllocator boolVarAlloc_,
                    int intWidth_) {
    super(astInfo_,boolVarAlloc_, intWidth_);
    }

    protected ExprTransl allocRelation(LeafId relId_) {
    // determine which dimension, if any, has scalar
    // multiplicity (i.e. if we hold all other dimension constant
    // and vary just this dimension, we will encounter exactly
    // one true tuple).
    //System.out.println("allocating leaf: " + _astInfo.getLeafRep(relId_).nodeString());
    MultiplicityExpr multExpr = _astInfo.getLeafMultiplicity(relId_);
    RelationType relType = _astInfo.getLeafType(relId_);
    int funcDim = -1;
    boolean funcIsOptionMult = false;
    if (multExpr instanceof SetMultExpr) {
        SetMultExpr setMultExpr = (SetMultExpr)multExpr;
        Multiplicity setMult = setMultExpr.getMult();
        if (!setMult.equals(Multiplicity.ONE) && !setMult.equals(Multiplicity.LONE))
            return super.allocRelation(relId_);
        //System.out.println("COMPACT set");
        funcDim = 0;
        funcIsOptionMult = setMult.equals(Multiplicity.LONE);
    } else {
        ArrowMultExpr arrowMult = (ArrowMultExpr)multExpr;
        Multiplicity leftMult = arrowMult.getLeft().getMult();
        Multiplicity rightMult = arrowMult.getRight().getMult();
        if (arrowMult.getRight().getType().toRelationType().numBasicTypes() != 1 ||
                (!rightMult.equals(Multiplicity.ONE) &&
                	!rightMult.equals(Multiplicity.LONE)))
            return super.allocRelation(relId_);
        //System.out.println("COMPACT relation");
        funcDim = relType.numBasicTypes()-1;
        funcIsOptionMult = rightMult.equals(Multiplicity.LONE);
    }
    int[] dims = (int[])relType.getScopes().clone();
    dims[funcDim] = Util.binaryLogUp(dims[funcDim] + (funcIsOptionMult ? 1 : 0));
    MultiDimArray formulas = new MultiDimArray(dims);
    Object[] formulasFlat = formulas.getFlatData();
    for (int i=0; i<formulasFlat.length; i++) {
        int freshBoolVar = _boolVarAllocator.allocBoolVar();
        //System.out.println("compalloc: " + freshBoolVar + " to " +
        //         _astInfo.getLeafRep(relId_).nodeString());
        formulasFlat[i] = BooleanFormula.makeLit(freshBoolVar);
    }

    ExprTransl result = new ExprTransl(relType, formulas, funcDim, funcIsOptionMult);

    // construct side conditions needed when the scope of a scalar set
    // is not a power of two; we represent the set by allocating Boolean
    // variables to the bits of a binary number which represents the one
    // nonzero tuple in the set; we add constraints that this binary
    // number is not greater than the scope.

    int[] enumOrder = new int[dims.length-1];
    {
        int n = 0;
        for (int i=0; i<dims.length; i++)
        if (i != funcDim)
            enumOrder[n++] = i;
    }


    IntTransl scopeTransl = IntTransl.fromIntConst(relType.getScopes()[funcDim] + (funcIsOptionMult ? 1 : 0));
    for (MultiDimIter scalarSetIter = new MultiDimIter(dims, enumOrder);
         scalarSetIter.hasNext();) {
        BooleanFormula[] funcDimBits = new BooleanFormula[dims[funcDim]];

        int[] scalarSetInds = (int[])scalarSetIter.next();
        for (int funcDimBit = 0; funcDimBit<dims[funcDim]; funcDimBit++) {
        scalarSetInds[funcDim] = funcDimBit;
        funcDimBits[funcDimBit] = result.getFuncTupleFormula(scalarSetInds);
        }
        IntTransl scalarTransl = new IntTransl(funcDimBits);
        _sideConditions.add(scalarTransl.lt(scopeTransl).formula);
    }

    return result;
    }  // allocRelation()

    /**
     * Return a side condition to be conjoined to the final formula.
     */
    public BooleanFormula getSideConditions() { return BooleanFormula.makeAnd(_sideConditions); }
}
